\begin{tabbing}
$\forall$\=$E$:Type, $T$, $V$:(Id$\rightarrow$Id$\rightarrow$Type), $M$:(IdLnk$\rightarrow$Id$\rightarrow$Type), ${\it pred?}$:($E$$\rightarrow$($E$+Unit)),\+
\\[0ex]${\it info}$:($E$$\rightarrow$(Id$\times$Id+(IdLnk$\times$$E$)$\times$Id)), ${\it init}$:($i$,$x$:Id$\rightarrow$$T$($i$,$x$)),
\\[0ex]${\it Trans}$:($i$:Id$\rightarrow$$k$:Knd$\rightarrow$kindcase($k$; $a$.$V$($i$,$a$); $l$,$t$.$M$($l$,$t$) )$\rightarrow$($x$:Id$\rightarrow$$T$($i$,$x$))$\rightarrow$($x$:Id$\rightarrow$$T$($i$,$x$))),
\\[0ex]${\it val}$:($e$:$E$$\rightarrow$kindcase(kind($e$); $a$.$V$(loc($e$),$a$); $l$,$t$.$M$($l$,$t$) )).
\-\\[0ex]($\forall$$e$:$E$. $\neg$first($e$) $\Rightarrow$ loc(pred($e$)) $=$ loc($e$) $\in$ Id)
\\[0ex]$\Rightarrow$ SWellFounded(pred!($e$;${\it e'}$))
\\[0ex]$\Rightarrow$ ($\forall$$e$:$E$. state\_when($e$) $\in$ $x$:Id$\rightarrow$$T$(loc($e$),$x$))
\end{tabbing}